The Runtime Complexity (full) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0) → 01
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, Z)
unquote(01) → 0
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)

Rewrite Strategy: FULL

(1) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(2) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0') → 01'
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, Z)
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)

S is empty.
Rewrite Strategy: FULL

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(4) Obligation:

TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0') → 01'
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, Z)
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)

Types:
sel :: s:0' → cons:nil → s:0'
s :: s:0' → s:0'
cons :: s:0' → cons:nil → cons:nil
0' :: s:0'
first :: s:0' → cons:nil → cons:nil
nil :: cons:nil
from :: s:0' → cons:nil
sel1 :: s:0' → cons:nil → 01':s1
quote :: s:0' → 01':s1
first1 :: s:0' → cons:nil → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
01' :: 01':s1
quote1 :: cons:nil → nil1:cons1
s1 :: 01':s1 → 01':s1
unquote :: 01':s1 → s:0'
unquote1 :: nil1:cons1 → cons:nil
fcons :: s:0' → cons:nil → cons:nil
hole_s:0'1_0 :: s:0'
hole_cons:nil2_0 :: cons:nil
hole_01':s13_0 :: 01':s1
hole_nil1:cons14_0 :: nil1:cons1
gen_s:0'5_0 :: Nat → s:0'
gen_cons:nil6_0 :: Nat → cons:nil
gen_01':s17_0 :: Nat → 01':s1
gen_nil1:cons18_0 :: Nat → nil1:cons1

(5) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
sel, first, from, sel1, quote, first1, quote1, unquote, unquote1

They will be analysed ascendingly in the following order:
sel1 = quote
quote < first1
quote < quote1
first1 < quote1
unquote < unquote1

(6) Obligation:

TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0') → 01'
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, Z)
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)

Types:
sel :: s:0' → cons:nil → s:0'
s :: s:0' → s:0'
cons :: s:0' → cons:nil → cons:nil
0' :: s:0'
first :: s:0' → cons:nil → cons:nil
nil :: cons:nil
from :: s:0' → cons:nil
sel1 :: s:0' → cons:nil → 01':s1
quote :: s:0' → 01':s1
first1 :: s:0' → cons:nil → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
01' :: 01':s1
quote1 :: cons:nil → nil1:cons1
s1 :: 01':s1 → 01':s1
unquote :: 01':s1 → s:0'
unquote1 :: nil1:cons1 → cons:nil
fcons :: s:0' → cons:nil → cons:nil
hole_s:0'1_0 :: s:0'
hole_cons:nil2_0 :: cons:nil
hole_01':s13_0 :: 01':s1
hole_nil1:cons14_0 :: nil1:cons1
gen_s:0'5_0 :: Nat → s:0'
gen_cons:nil6_0 :: Nat → cons:nil
gen_01':s17_0 :: Nat → 01':s1
gen_nil1:cons18_0 :: Nat → nil1:cons1

Generator Equations:
gen_s:0'5_0(0) ⇔ 0'
gen_s:0'5_0(+(x, 1)) ⇔ s(gen_s:0'5_0(x))
gen_cons:nil6_0(0) ⇔ nil
gen_cons:nil6_0(+(x, 1)) ⇔ cons(0', gen_cons:nil6_0(x))
gen_01':s17_0(0) ⇔ 01'
gen_01':s17_0(+(x, 1)) ⇔ s1(gen_01':s17_0(x))
gen_nil1:cons18_0(0) ⇔ nil1
gen_nil1:cons18_0(+(x, 1)) ⇔ cons1(01', gen_nil1:cons18_0(x))

The following defined symbols remain to be analysed:
sel, first, from, sel1, quote, first1, quote1, unquote, unquote1

They will be analysed ascendingly in the following order:
sel1 = quote
quote < first1
quote < quote1
first1 < quote1
unquote < unquote1

(7) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)

Induction Base:
sel(gen_s:0'5_0(0), gen_cons:nil6_0(+(1, 0))) →_R^Ω(1)
0'

Induction Step:
sel(gen_s:0'5_0(+(n10_0, 1)), gen_cons:nil6_0(+(1, +(n10_0, 1)))) →_R^Ω(1)
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) →_IH
gen_s:0'5_0(0)

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(8) Complex Obligation (BEST)

(9) Obligation:

TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0') → 01'
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, Z)
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)

Types:
sel :: s:0' → cons:nil → s:0'
s :: s:0' → s:0'
cons :: s:0' → cons:nil → cons:nil
0' :: s:0'
first :: s:0' → cons:nil → cons:nil
nil :: cons:nil
from :: s:0' → cons:nil
sel1 :: s:0' → cons:nil → 01':s1
quote :: s:0' → 01':s1
first1 :: s:0' → cons:nil → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
01' :: 01':s1
quote1 :: cons:nil → nil1:cons1
s1 :: 01':s1 → 01':s1
unquote :: 01':s1 → s:0'
unquote1 :: nil1:cons1 → cons:nil
fcons :: s:0' → cons:nil → cons:nil
hole_s:0'1_0 :: s:0'
hole_cons:nil2_0 :: cons:nil
hole_01':s13_0 :: 01':s1
hole_nil1:cons14_0 :: nil1:cons1
gen_s:0'5_0 :: Nat → s:0'
gen_cons:nil6_0 :: Nat → cons:nil
gen_01':s17_0 :: Nat → 01':s1
gen_nil1:cons18_0 :: Nat → nil1:cons1

Lemmas:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)

Generator Equations:
gen_s:0'5_0(0) ⇔ 0'
gen_s:0'5_0(+(x, 1)) ⇔ s(gen_s:0'5_0(x))
gen_cons:nil6_0(0) ⇔ nil
gen_cons:nil6_0(+(x, 1)) ⇔ cons(0', gen_cons:nil6_0(x))
gen_01':s17_0(0) ⇔ 01'
gen_01':s17_0(+(x, 1)) ⇔ s1(gen_01':s17_0(x))
gen_nil1:cons18_0(0) ⇔ nil1
gen_nil1:cons18_0(+(x, 1)) ⇔ cons1(01', gen_nil1:cons18_0(x))

The following defined symbols remain to be analysed:
first, from, sel1, quote, first1, quote1, unquote, unquote1

They will be analysed ascendingly in the following order:
sel1 = quote
quote < first1
quote < quote1
first1 < quote1
unquote < unquote1

(10) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
first(gen_s:0'5_0(n464_0), gen_cons:nil6_0(n464_0)) → gen_cons:nil6_0(n464_0), rt ∈ Ω(1 + n464₀)

Induction Base:
first(gen_s:0'5_0(0), gen_cons:nil6_0(0)) →_R^Ω(1)
nil

Induction Step:
first(gen_s:0'5_0(+(n464_0, 1)), gen_cons:nil6_0(+(n464_0, 1))) →_R^Ω(1)
cons(0', first(gen_s:0'5_0(n464_0), gen_cons:nil6_0(n464_0))) →_IH
cons(0', gen_cons:nil6_0(c465_0))

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(11) Complex Obligation (BEST)

(12) Obligation:

TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0') → 01'
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, Z)
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)

Types:
sel :: s:0' → cons:nil → s:0'
s :: s:0' → s:0'
cons :: s:0' → cons:nil → cons:nil
0' :: s:0'
first :: s:0' → cons:nil → cons:nil
nil :: cons:nil
from :: s:0' → cons:nil
sel1 :: s:0' → cons:nil → 01':s1
quote :: s:0' → 01':s1
first1 :: s:0' → cons:nil → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
01' :: 01':s1
quote1 :: cons:nil → nil1:cons1
s1 :: 01':s1 → 01':s1
unquote :: 01':s1 → s:0'
unquote1 :: nil1:cons1 → cons:nil
fcons :: s:0' → cons:nil → cons:nil
hole_s:0'1_0 :: s:0'
hole_cons:nil2_0 :: cons:nil
hole_01':s13_0 :: 01':s1
hole_nil1:cons14_0 :: nil1:cons1
gen_s:0'5_0 :: Nat → s:0'
gen_cons:nil6_0 :: Nat → cons:nil
gen_01':s17_0 :: Nat → 01':s1
gen_nil1:cons18_0 :: Nat → nil1:cons1

Lemmas:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)
first(gen_s:0'5_0(n464_0), gen_cons:nil6_0(n464_0)) → gen_cons:nil6_0(n464_0), rt ∈ Ω(1 + n464₀)

Generator Equations:
gen_s:0'5_0(0) ⇔ 0'
gen_s:0'5_0(+(x, 1)) ⇔ s(gen_s:0'5_0(x))
gen_cons:nil6_0(0) ⇔ nil
gen_cons:nil6_0(+(x, 1)) ⇔ cons(0', gen_cons:nil6_0(x))
gen_01':s17_0(0) ⇔ 01'
gen_01':s17_0(+(x, 1)) ⇔ s1(gen_01':s17_0(x))
gen_nil1:cons18_0(0) ⇔ nil1
gen_nil1:cons18_0(+(x, 1)) ⇔ cons1(01', gen_nil1:cons18_0(x))

The following defined symbols remain to be analysed:
from, sel1, quote, first1, quote1, unquote, unquote1

They will be analysed ascendingly in the following order:
sel1 = quote
quote < first1
quote < quote1
first1 < quote1
unquote < unquote1

(13) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol from.

(14) Obligation:

TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0') → 01'
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, Z)
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)

Types:
sel :: s:0' → cons:nil → s:0'
s :: s:0' → s:0'
cons :: s:0' → cons:nil → cons:nil
0' :: s:0'
first :: s:0' → cons:nil → cons:nil
nil :: cons:nil
from :: s:0' → cons:nil
sel1 :: s:0' → cons:nil → 01':s1
quote :: s:0' → 01':s1
first1 :: s:0' → cons:nil → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
01' :: 01':s1
quote1 :: cons:nil → nil1:cons1
s1 :: 01':s1 → 01':s1
unquote :: 01':s1 → s:0'
unquote1 :: nil1:cons1 → cons:nil
fcons :: s:0' → cons:nil → cons:nil
hole_s:0'1_0 :: s:0'
hole_cons:nil2_0 :: cons:nil
hole_01':s13_0 :: 01':s1
hole_nil1:cons14_0 :: nil1:cons1
gen_s:0'5_0 :: Nat → s:0'
gen_cons:nil6_0 :: Nat → cons:nil
gen_01':s17_0 :: Nat → 01':s1
gen_nil1:cons18_0 :: Nat → nil1:cons1

Lemmas:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)
first(gen_s:0'5_0(n464_0), gen_cons:nil6_0(n464_0)) → gen_cons:nil6_0(n464_0), rt ∈ Ω(1 + n464₀)

Generator Equations:
gen_s:0'5_0(0) ⇔ 0'
gen_s:0'5_0(+(x, 1)) ⇔ s(gen_s:0'5_0(x))
gen_cons:nil6_0(0) ⇔ nil
gen_cons:nil6_0(+(x, 1)) ⇔ cons(0', gen_cons:nil6_0(x))
gen_01':s17_0(0) ⇔ 01'
gen_01':s17_0(+(x, 1)) ⇔ s1(gen_01':s17_0(x))
gen_nil1:cons18_0(0) ⇔ nil1
gen_nil1:cons18_0(+(x, 1)) ⇔ cons1(01', gen_nil1:cons18_0(x))

The following defined symbols remain to be analysed:
unquote, sel1, quote, first1, quote1, unquote1

They will be analysed ascendingly in the following order:
sel1 = quote
quote < first1
quote < quote1
first1 < quote1
unquote < unquote1

(15) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
unquote(gen_01':s17_0(n945_0)) → gen_s:0'5_0(n945_0), rt ∈ Ω(1 + n945₀)

Induction Base:
unquote(gen_01':s17_0(0)) →_R^Ω(1)
0'

Induction Step:
unquote(gen_01':s17_0(+(n945_0, 1))) →_R^Ω(1)
s(unquote(gen_01':s17_0(n945_0))) →_IH
s(gen_s:0'5_0(c946_0))

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(16) Complex Obligation (BEST)

(17) Obligation:

TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0') → 01'
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, Z)
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)

Types:
sel :: s:0' → cons:nil → s:0'
s :: s:0' → s:0'
cons :: s:0' → cons:nil → cons:nil
0' :: s:0'
first :: s:0' → cons:nil → cons:nil
nil :: cons:nil
from :: s:0' → cons:nil
sel1 :: s:0' → cons:nil → 01':s1
quote :: s:0' → 01':s1
first1 :: s:0' → cons:nil → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
01' :: 01':s1
quote1 :: cons:nil → nil1:cons1
s1 :: 01':s1 → 01':s1
unquote :: 01':s1 → s:0'
unquote1 :: nil1:cons1 → cons:nil
fcons :: s:0' → cons:nil → cons:nil
hole_s:0'1_0 :: s:0'
hole_cons:nil2_0 :: cons:nil
hole_01':s13_0 :: 01':s1
hole_nil1:cons14_0 :: nil1:cons1
gen_s:0'5_0 :: Nat → s:0'
gen_cons:nil6_0 :: Nat → cons:nil
gen_01':s17_0 :: Nat → 01':s1
gen_nil1:cons18_0 :: Nat → nil1:cons1

Lemmas:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)
first(gen_s:0'5_0(n464_0), gen_cons:nil6_0(n464_0)) → gen_cons:nil6_0(n464_0), rt ∈ Ω(1 + n464₀)
unquote(gen_01':s17_0(n945_0)) → gen_s:0'5_0(n945_0), rt ∈ Ω(1 + n945₀)

Generator Equations:
gen_s:0'5_0(0) ⇔ 0'
gen_s:0'5_0(+(x, 1)) ⇔ s(gen_s:0'5_0(x))
gen_cons:nil6_0(0) ⇔ nil
gen_cons:nil6_0(+(x, 1)) ⇔ cons(0', gen_cons:nil6_0(x))
gen_01':s17_0(0) ⇔ 01'
gen_01':s17_0(+(x, 1)) ⇔ s1(gen_01':s17_0(x))
gen_nil1:cons18_0(0) ⇔ nil1
gen_nil1:cons18_0(+(x, 1)) ⇔ cons1(01', gen_nil1:cons18_0(x))

The following defined symbols remain to be analysed:
unquote1, sel1, quote, first1, quote1

They will be analysed ascendingly in the following order:
sel1 = quote
quote < first1
quote < quote1
first1 < quote1

(18) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
unquote1(gen_nil1:cons18_0(n1203_0)) → gen_cons:nil6_0(n1203_0), rt ∈ Ω(1 + n1203₀)

Induction Base:
unquote1(gen_nil1:cons18_0(0)) →_R^Ω(1)
nil

Induction Step:
unquote1(gen_nil1:cons18_0(+(n1203_0, 1))) →_R^Ω(1)
fcons(unquote(01'), unquote1(gen_nil1:cons18_0(n1203_0))) →_L^Ω(1)
fcons(gen_s:0'5_0(0), unquote1(gen_nil1:cons18_0(n1203_0))) →_IH
fcons(gen_s:0'5_0(0), gen_cons:nil6_0(c1204_0)) →_R^Ω(1)
cons(gen_s:0'5_0(0), gen_cons:nil6_0(n1203_0))

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(19) Complex Obligation (BEST)

(20) Obligation:

TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0') → 01'
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, Z)
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)

Types:
sel :: s:0' → cons:nil → s:0'
s :: s:0' → s:0'
cons :: s:0' → cons:nil → cons:nil
0' :: s:0'
first :: s:0' → cons:nil → cons:nil
nil :: cons:nil
from :: s:0' → cons:nil
sel1 :: s:0' → cons:nil → 01':s1
quote :: s:0' → 01':s1
first1 :: s:0' → cons:nil → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
01' :: 01':s1
quote1 :: cons:nil → nil1:cons1
s1 :: 01':s1 → 01':s1
unquote :: 01':s1 → s:0'
unquote1 :: nil1:cons1 → cons:nil
fcons :: s:0' → cons:nil → cons:nil
hole_s:0'1_0 :: s:0'
hole_cons:nil2_0 :: cons:nil
hole_01':s13_0 :: 01':s1
hole_nil1:cons14_0 :: nil1:cons1
gen_s:0'5_0 :: Nat → s:0'
gen_cons:nil6_0 :: Nat → cons:nil
gen_01':s17_0 :: Nat → 01':s1
gen_nil1:cons18_0 :: Nat → nil1:cons1

Lemmas:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)
first(gen_s:0'5_0(n464_0), gen_cons:nil6_0(n464_0)) → gen_cons:nil6_0(n464_0), rt ∈ Ω(1 + n464₀)
unquote(gen_01':s17_0(n945_0)) → gen_s:0'5_0(n945_0), rt ∈ Ω(1 + n945₀)
unquote1(gen_nil1:cons18_0(n1203_0)) → gen_cons:nil6_0(n1203_0), rt ∈ Ω(1 + n1203₀)

Generator Equations:
gen_s:0'5_0(0) ⇔ 0'
gen_s:0'5_0(+(x, 1)) ⇔ s(gen_s:0'5_0(x))
gen_cons:nil6_0(0) ⇔ nil
gen_cons:nil6_0(+(x, 1)) ⇔ cons(0', gen_cons:nil6_0(x))
gen_01':s17_0(0) ⇔ 01'
gen_01':s17_0(+(x, 1)) ⇔ s1(gen_01':s17_0(x))
gen_nil1:cons18_0(0) ⇔ nil1
gen_nil1:cons18_0(+(x, 1)) ⇔ cons1(01', gen_nil1:cons18_0(x))

The following defined symbols remain to be analysed:
quote, sel1, first1, quote1

They will be analysed ascendingly in the following order:
sel1 = quote
quote < first1
quote < quote1
first1 < quote1

(21) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
quote(gen_s:0'5_0(n1846_0)) → gen_01':s17_0(n1846_0), rt ∈ Ω(1 + n1846₀)

Induction Base:
quote(gen_s:0'5_0(0)) →_R^Ω(1)
01'

Induction Step:
quote(gen_s:0'5_0(+(n1846_0, 1))) →_R^Ω(1)
s1(quote(gen_s:0'5_0(n1846_0))) →_IH
s1(gen_01':s17_0(c1847_0))

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(22) Complex Obligation (BEST)

(23) Obligation:

TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0') → 01'
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, Z)
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)

Types:
sel :: s:0' → cons:nil → s:0'
s :: s:0' → s:0'
cons :: s:0' → cons:nil → cons:nil
0' :: s:0'
first :: s:0' → cons:nil → cons:nil
nil :: cons:nil
from :: s:0' → cons:nil
sel1 :: s:0' → cons:nil → 01':s1
quote :: s:0' → 01':s1
first1 :: s:0' → cons:nil → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
01' :: 01':s1
quote1 :: cons:nil → nil1:cons1
s1 :: 01':s1 → 01':s1
unquote :: 01':s1 → s:0'
unquote1 :: nil1:cons1 → cons:nil
fcons :: s:0' → cons:nil → cons:nil
hole_s:0'1_0 :: s:0'
hole_cons:nil2_0 :: cons:nil
hole_01':s13_0 :: 01':s1
hole_nil1:cons14_0 :: nil1:cons1
gen_s:0'5_0 :: Nat → s:0'
gen_cons:nil6_0 :: Nat → cons:nil
gen_01':s17_0 :: Nat → 01':s1
gen_nil1:cons18_0 :: Nat → nil1:cons1

Lemmas:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)
first(gen_s:0'5_0(n464_0), gen_cons:nil6_0(n464_0)) → gen_cons:nil6_0(n464_0), rt ∈ Ω(1 + n464₀)
unquote(gen_01':s17_0(n945_0)) → gen_s:0'5_0(n945_0), rt ∈ Ω(1 + n945₀)
unquote1(gen_nil1:cons18_0(n1203_0)) → gen_cons:nil6_0(n1203_0), rt ∈ Ω(1 + n1203₀)
quote(gen_s:0'5_0(n1846_0)) → gen_01':s17_0(n1846_0), rt ∈ Ω(1 + n1846₀)

Generator Equations:
gen_s:0'5_0(0) ⇔ 0'
gen_s:0'5_0(+(x, 1)) ⇔ s(gen_s:0'5_0(x))
gen_cons:nil6_0(0) ⇔ nil
gen_cons:nil6_0(+(x, 1)) ⇔ cons(0', gen_cons:nil6_0(x))
gen_01':s17_0(0) ⇔ 01'
gen_01':s17_0(+(x, 1)) ⇔ s1(gen_01':s17_0(x))
gen_nil1:cons18_0(0) ⇔ nil1
gen_nil1:cons18_0(+(x, 1)) ⇔ cons1(01', gen_nil1:cons18_0(x))

The following defined symbols remain to be analysed:
sel1, first1, quote1

They will be analysed ascendingly in the following order:
sel1 = quote
quote < first1
quote < quote1
first1 < quote1

(24) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
sel1(gen_s:0'5_0(n2282_0), gen_cons:nil6_0(+(1, n2282_0))) → gen_01':s17_0(0), rt ∈ Ω(1 + n2282₀)

Induction Base:
sel1(gen_s:0'5_0(0), gen_cons:nil6_0(+(1, 0))) →_R^Ω(1)
quote(0') →_L^Ω(1)
gen_01':s17_0(0)

Induction Step:
sel1(gen_s:0'5_0(+(n2282_0, 1)), gen_cons:nil6_0(+(1, +(n2282_0, 1)))) →_R^Ω(1)
sel1(gen_s:0'5_0(n2282_0), gen_cons:nil6_0(+(1, n2282_0))) →_IH
gen_01':s17_0(0)

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(25) Complex Obligation (BEST)

(26) Obligation:

TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0') → 01'
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, Z)
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)

Types:
sel :: s:0' → cons:nil → s:0'
s :: s:0' → s:0'
cons :: s:0' → cons:nil → cons:nil
0' :: s:0'
first :: s:0' → cons:nil → cons:nil
nil :: cons:nil
from :: s:0' → cons:nil
sel1 :: s:0' → cons:nil → 01':s1
quote :: s:0' → 01':s1
first1 :: s:0' → cons:nil → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
01' :: 01':s1
quote1 :: cons:nil → nil1:cons1
s1 :: 01':s1 → 01':s1
unquote :: 01':s1 → s:0'
unquote1 :: nil1:cons1 → cons:nil
fcons :: s:0' → cons:nil → cons:nil
hole_s:0'1_0 :: s:0'
hole_cons:nil2_0 :: cons:nil
hole_01':s13_0 :: 01':s1
hole_nil1:cons14_0 :: nil1:cons1
gen_s:0'5_0 :: Nat → s:0'
gen_cons:nil6_0 :: Nat → cons:nil
gen_01':s17_0 :: Nat → 01':s1
gen_nil1:cons18_0 :: Nat → nil1:cons1

Lemmas:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)
first(gen_s:0'5_0(n464_0), gen_cons:nil6_0(n464_0)) → gen_cons:nil6_0(n464_0), rt ∈ Ω(1 + n464₀)
unquote(gen_01':s17_0(n945_0)) → gen_s:0'5_0(n945_0), rt ∈ Ω(1 + n945₀)
unquote1(gen_nil1:cons18_0(n1203_0)) → gen_cons:nil6_0(n1203_0), rt ∈ Ω(1 + n1203₀)
quote(gen_s:0'5_0(n1846_0)) → gen_01':s17_0(n1846_0), rt ∈ Ω(1 + n1846₀)
sel1(gen_s:0'5_0(n2282_0), gen_cons:nil6_0(+(1, n2282_0))) → gen_01':s17_0(0), rt ∈ Ω(1 + n2282₀)

Generator Equations:
gen_s:0'5_0(0) ⇔ 0'
gen_s:0'5_0(+(x, 1)) ⇔ s(gen_s:0'5_0(x))
gen_cons:nil6_0(0) ⇔ nil
gen_cons:nil6_0(+(x, 1)) ⇔ cons(0', gen_cons:nil6_0(x))
gen_01':s17_0(0) ⇔ 01'
gen_01':s17_0(+(x, 1)) ⇔ s1(gen_01':s17_0(x))
gen_nil1:cons18_0(0) ⇔ nil1
gen_nil1:cons18_0(+(x, 1)) ⇔ cons1(01', gen_nil1:cons18_0(x))

The following defined symbols remain to be analysed:
quote, first1, quote1

They will be analysed ascendingly in the following order:
sel1 = quote
quote < first1
quote < quote1
first1 < quote1

(27) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
quote(gen_s:0'5_0(n2813_0)) → gen_01':s17_0(n2813_0), rt ∈ Ω(1 + n2813₀)

Induction Base:
quote(gen_s:0'5_0(0)) →_R^Ω(1)
01'

Induction Step:
quote(gen_s:0'5_0(+(n2813_0, 1))) →_R^Ω(1)
s1(quote(gen_s:0'5_0(n2813_0))) →_IH
s1(gen_01':s17_0(c2814_0))

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(28) Complex Obligation (BEST)

(29) Obligation:

TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0') → 01'
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, Z)
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)

Types:
sel :: s:0' → cons:nil → s:0'
s :: s:0' → s:0'
cons :: s:0' → cons:nil → cons:nil
0' :: s:0'
first :: s:0' → cons:nil → cons:nil
nil :: cons:nil
from :: s:0' → cons:nil
sel1 :: s:0' → cons:nil → 01':s1
quote :: s:0' → 01':s1
first1 :: s:0' → cons:nil → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
01' :: 01':s1
quote1 :: cons:nil → nil1:cons1
s1 :: 01':s1 → 01':s1
unquote :: 01':s1 → s:0'
unquote1 :: nil1:cons1 → cons:nil
fcons :: s:0' → cons:nil → cons:nil
hole_s:0'1_0 :: s:0'
hole_cons:nil2_0 :: cons:nil
hole_01':s13_0 :: 01':s1
hole_nil1:cons14_0 :: nil1:cons1
gen_s:0'5_0 :: Nat → s:0'
gen_cons:nil6_0 :: Nat → cons:nil
gen_01':s17_0 :: Nat → 01':s1
gen_nil1:cons18_0 :: Nat → nil1:cons1

Lemmas:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)
first(gen_s:0'5_0(n464_0), gen_cons:nil6_0(n464_0)) → gen_cons:nil6_0(n464_0), rt ∈ Ω(1 + n464₀)
unquote(gen_01':s17_0(n945_0)) → gen_s:0'5_0(n945_0), rt ∈ Ω(1 + n945₀)
unquote1(gen_nil1:cons18_0(n1203_0)) → gen_cons:nil6_0(n1203_0), rt ∈ Ω(1 + n1203₀)
quote(gen_s:0'5_0(n2813_0)) → gen_01':s17_0(n2813_0), rt ∈ Ω(1 + n2813₀)
sel1(gen_s:0'5_0(n2282_0), gen_cons:nil6_0(+(1, n2282_0))) → gen_01':s17_0(0), rt ∈ Ω(1 + n2282₀)

Generator Equations:
gen_s:0'5_0(0) ⇔ 0'
gen_s:0'5_0(+(x, 1)) ⇔ s(gen_s:0'5_0(x))
gen_cons:nil6_0(0) ⇔ nil
gen_cons:nil6_0(+(x, 1)) ⇔ cons(0', gen_cons:nil6_0(x))
gen_01':s17_0(0) ⇔ 01'
gen_01':s17_0(+(x, 1)) ⇔ s1(gen_01':s17_0(x))
gen_nil1:cons18_0(0) ⇔ nil1
gen_nil1:cons18_0(+(x, 1)) ⇔ cons1(01', gen_nil1:cons18_0(x))

The following defined symbols remain to be analysed:
first1, quote1

They will be analysed ascendingly in the following order:
first1 < quote1

(30) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
first1(gen_s:0'5_0(n3253_0), gen_cons:nil6_0(n3253_0)) → gen_nil1:cons18_0(n3253_0), rt ∈ Ω(1 + n3253₀)

Induction Base:
first1(gen_s:0'5_0(0), gen_cons:nil6_0(0)) →_R^Ω(1)
nil1

Induction Step:
first1(gen_s:0'5_0(+(n3253_0, 1)), gen_cons:nil6_0(+(n3253_0, 1))) →_R^Ω(1)
cons1(quote(0'), first1(gen_s:0'5_0(n3253_0), gen_cons:nil6_0(n3253_0))) →_L^Ω(1)
cons1(gen_01':s17_0(0), first1(gen_s:0'5_0(n3253_0), gen_cons:nil6_0(n3253_0))) →_IH
cons1(gen_01':s17_0(0), gen_nil1:cons18_0(c3254_0))

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(31) Complex Obligation (BEST)

(32) Obligation:

TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0') → 01'
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, Z)
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)

Types:
sel :: s:0' → cons:nil → s:0'
s :: s:0' → s:0'
cons :: s:0' → cons:nil → cons:nil
0' :: s:0'
first :: s:0' → cons:nil → cons:nil
nil :: cons:nil
from :: s:0' → cons:nil
sel1 :: s:0' → cons:nil → 01':s1
quote :: s:0' → 01':s1
first1 :: s:0' → cons:nil → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
01' :: 01':s1
quote1 :: cons:nil → nil1:cons1
s1 :: 01':s1 → 01':s1
unquote :: 01':s1 → s:0'
unquote1 :: nil1:cons1 → cons:nil
fcons :: s:0' → cons:nil → cons:nil
hole_s:0'1_0 :: s:0'
hole_cons:nil2_0 :: cons:nil
hole_01':s13_0 :: 01':s1
hole_nil1:cons14_0 :: nil1:cons1
gen_s:0'5_0 :: Nat → s:0'
gen_cons:nil6_0 :: Nat → cons:nil
gen_01':s17_0 :: Nat → 01':s1
gen_nil1:cons18_0 :: Nat → nil1:cons1

Lemmas:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)
first(gen_s:0'5_0(n464_0), gen_cons:nil6_0(n464_0)) → gen_cons:nil6_0(n464_0), rt ∈ Ω(1 + n464₀)
unquote(gen_01':s17_0(n945_0)) → gen_s:0'5_0(n945_0), rt ∈ Ω(1 + n945₀)
unquote1(gen_nil1:cons18_0(n1203_0)) → gen_cons:nil6_0(n1203_0), rt ∈ Ω(1 + n1203₀)
quote(gen_s:0'5_0(n2813_0)) → gen_01':s17_0(n2813_0), rt ∈ Ω(1 + n2813₀)
sel1(gen_s:0'5_0(n2282_0), gen_cons:nil6_0(+(1, n2282_0))) → gen_01':s17_0(0), rt ∈ Ω(1 + n2282₀)
first1(gen_s:0'5_0(n3253_0), gen_cons:nil6_0(n3253_0)) → gen_nil1:cons18_0(n3253_0), rt ∈ Ω(1 + n3253₀)

Generator Equations:
gen_s:0'5_0(0) ⇔ 0'
gen_s:0'5_0(+(x, 1)) ⇔ s(gen_s:0'5_0(x))
gen_cons:nil6_0(0) ⇔ nil
gen_cons:nil6_0(+(x, 1)) ⇔ cons(0', gen_cons:nil6_0(x))
gen_01':s17_0(0) ⇔ 01'
gen_01':s17_0(+(x, 1)) ⇔ s1(gen_01':s17_0(x))
gen_nil1:cons18_0(0) ⇔ nil1
gen_nil1:cons18_0(+(x, 1)) ⇔ cons1(01', gen_nil1:cons18_0(x))

The following defined symbols remain to be analysed:
quote1

(33) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
quote1(gen_cons:nil6_0(n3927_0)) → gen_nil1:cons18_0(n3927_0), rt ∈ Ω(1 + n3927₀)

Induction Base:
quote1(gen_cons:nil6_0(0)) →_R^Ω(1)
nil1

Induction Step:
quote1(gen_cons:nil6_0(+(n3927_0, 1))) →_R^Ω(1)
cons1(quote(0'), quote1(gen_cons:nil6_0(n3927_0))) →_L^Ω(1)
cons1(gen_01':s17_0(0), quote1(gen_cons:nil6_0(n3927_0))) →_IH
cons1(gen_01':s17_0(0), gen_nil1:cons18_0(c3928_0))

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(34) Complex Obligation (BEST)

(35) Obligation:

TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0') → 01'
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, Z)
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)

Types:
sel :: s:0' → cons:nil → s:0'
s :: s:0' → s:0'
cons :: s:0' → cons:nil → cons:nil
0' :: s:0'
first :: s:0' → cons:nil → cons:nil
nil :: cons:nil
from :: s:0' → cons:nil
sel1 :: s:0' → cons:nil → 01':s1
quote :: s:0' → 01':s1
first1 :: s:0' → cons:nil → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
01' :: 01':s1
quote1 :: cons:nil → nil1:cons1
s1 :: 01':s1 → 01':s1
unquote :: 01':s1 → s:0'
unquote1 :: nil1:cons1 → cons:nil
fcons :: s:0' → cons:nil → cons:nil
hole_s:0'1_0 :: s:0'
hole_cons:nil2_0 :: cons:nil
hole_01':s13_0 :: 01':s1
hole_nil1:cons14_0 :: nil1:cons1
gen_s:0'5_0 :: Nat → s:0'
gen_cons:nil6_0 :: Nat → cons:nil
gen_01':s17_0 :: Nat → 01':s1
gen_nil1:cons18_0 :: Nat → nil1:cons1

Lemmas:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)
first(gen_s:0'5_0(n464_0), gen_cons:nil6_0(n464_0)) → gen_cons:nil6_0(n464_0), rt ∈ Ω(1 + n464₀)
unquote(gen_01':s17_0(n945_0)) → gen_s:0'5_0(n945_0), rt ∈ Ω(1 + n945₀)
unquote1(gen_nil1:cons18_0(n1203_0)) → gen_cons:nil6_0(n1203_0), rt ∈ Ω(1 + n1203₀)
quote(gen_s:0'5_0(n2813_0)) → gen_01':s17_0(n2813_0), rt ∈ Ω(1 + n2813₀)
sel1(gen_s:0'5_0(n2282_0), gen_cons:nil6_0(+(1, n2282_0))) → gen_01':s17_0(0), rt ∈ Ω(1 + n2282₀)
first1(gen_s:0'5_0(n3253_0), gen_cons:nil6_0(n3253_0)) → gen_nil1:cons18_0(n3253_0), rt ∈ Ω(1 + n3253₀)
quote1(gen_cons:nil6_0(n3927_0)) → gen_nil1:cons18_0(n3927_0), rt ∈ Ω(1 + n3927₀)

Generator Equations:
gen_s:0'5_0(0) ⇔ 0'
gen_s:0'5_0(+(x, 1)) ⇔ s(gen_s:0'5_0(x))
gen_cons:nil6_0(0) ⇔ nil
gen_cons:nil6_0(+(x, 1)) ⇔ cons(0', gen_cons:nil6_0(x))
gen_01':s17_0(0) ⇔ 01'
gen_01':s17_0(+(x, 1)) ⇔ s1(gen_01':s17_0(x))
gen_nil1:cons18_0(0) ⇔ nil1
gen_nil1:cons18_0(+(x, 1)) ⇔ cons1(01', gen_nil1:cons18_0(x))

No more defined symbols left to analyse.

(36) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)

(37) BOUNDS(n^1, INF)

(38) Obligation:

TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0') → 01'
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, Z)
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)

Types:
sel :: s:0' → cons:nil → s:0'
s :: s:0' → s:0'
cons :: s:0' → cons:nil → cons:nil
0' :: s:0'
first :: s:0' → cons:nil → cons:nil
nil :: cons:nil
from :: s:0' → cons:nil
sel1 :: s:0' → cons:nil → 01':s1
quote :: s:0' → 01':s1
first1 :: s:0' → cons:nil → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
01' :: 01':s1
quote1 :: cons:nil → nil1:cons1
s1 :: 01':s1 → 01':s1
unquote :: 01':s1 → s:0'
unquote1 :: nil1:cons1 → cons:nil
fcons :: s:0' → cons:nil → cons:nil
hole_s:0'1_0 :: s:0'
hole_cons:nil2_0 :: cons:nil
hole_01':s13_0 :: 01':s1
hole_nil1:cons14_0 :: nil1:cons1
gen_s:0'5_0 :: Nat → s:0'
gen_cons:nil6_0 :: Nat → cons:nil
gen_01':s17_0 :: Nat → 01':s1
gen_nil1:cons18_0 :: Nat → nil1:cons1

Lemmas:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)
first(gen_s:0'5_0(n464_0), gen_cons:nil6_0(n464_0)) → gen_cons:nil6_0(n464_0), rt ∈ Ω(1 + n464₀)
unquote(gen_01':s17_0(n945_0)) → gen_s:0'5_0(n945_0), rt ∈ Ω(1 + n945₀)
unquote1(gen_nil1:cons18_0(n1203_0)) → gen_cons:nil6_0(n1203_0), rt ∈ Ω(1 + n1203₀)
quote(gen_s:0'5_0(n2813_0)) → gen_01':s17_0(n2813_0), rt ∈ Ω(1 + n2813₀)
sel1(gen_s:0'5_0(n2282_0), gen_cons:nil6_0(+(1, n2282_0))) → gen_01':s17_0(0), rt ∈ Ω(1 + n2282₀)
first1(gen_s:0'5_0(n3253_0), gen_cons:nil6_0(n3253_0)) → gen_nil1:cons18_0(n3253_0), rt ∈ Ω(1 + n3253₀)
quote1(gen_cons:nil6_0(n3927_0)) → gen_nil1:cons18_0(n3927_0), rt ∈ Ω(1 + n3927₀)

Generator Equations:
gen_s:0'5_0(0) ⇔ 0'
gen_s:0'5_0(+(x, 1)) ⇔ s(gen_s:0'5_0(x))
gen_cons:nil6_0(0) ⇔ nil
gen_cons:nil6_0(+(x, 1)) ⇔ cons(0', gen_cons:nil6_0(x))
gen_01':s17_0(0) ⇔ 01'
gen_01':s17_0(+(x, 1)) ⇔ s1(gen_01':s17_0(x))
gen_nil1:cons18_0(0) ⇔ nil1
gen_nil1:cons18_0(+(x, 1)) ⇔ cons1(01', gen_nil1:cons18_0(x))

No more defined symbols left to analyse.

(39) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)

(40) BOUNDS(n^1, INF)

(41) Obligation:

TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0') → 01'
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, Z)
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)

Types:
sel :: s:0' → cons:nil → s:0'
s :: s:0' → s:0'
cons :: s:0' → cons:nil → cons:nil
0' :: s:0'
first :: s:0' → cons:nil → cons:nil
nil :: cons:nil
from :: s:0' → cons:nil
sel1 :: s:0' → cons:nil → 01':s1
quote :: s:0' → 01':s1
first1 :: s:0' → cons:nil → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
01' :: 01':s1
quote1 :: cons:nil → nil1:cons1
s1 :: 01':s1 → 01':s1
unquote :: 01':s1 → s:0'
unquote1 :: nil1:cons1 → cons:nil
fcons :: s:0' → cons:nil → cons:nil
hole_s:0'1_0 :: s:0'
hole_cons:nil2_0 :: cons:nil
hole_01':s13_0 :: 01':s1
hole_nil1:cons14_0 :: nil1:cons1
gen_s:0'5_0 :: Nat → s:0'
gen_cons:nil6_0 :: Nat → cons:nil
gen_01':s17_0 :: Nat → 01':s1
gen_nil1:cons18_0 :: Nat → nil1:cons1

Lemmas:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)
first(gen_s:0'5_0(n464_0), gen_cons:nil6_0(n464_0)) → gen_cons:nil6_0(n464_0), rt ∈ Ω(1 + n464₀)
unquote(gen_01':s17_0(n945_0)) → gen_s:0'5_0(n945_0), rt ∈ Ω(1 + n945₀)
unquote1(gen_nil1:cons18_0(n1203_0)) → gen_cons:nil6_0(n1203_0), rt ∈ Ω(1 + n1203₀)
quote(gen_s:0'5_0(n2813_0)) → gen_01':s17_0(n2813_0), rt ∈ Ω(1 + n2813₀)
sel1(gen_s:0'5_0(n2282_0), gen_cons:nil6_0(+(1, n2282_0))) → gen_01':s17_0(0), rt ∈ Ω(1 + n2282₀)
first1(gen_s:0'5_0(n3253_0), gen_cons:nil6_0(n3253_0)) → gen_nil1:cons18_0(n3253_0), rt ∈ Ω(1 + n3253₀)

Generator Equations:
gen_s:0'5_0(0) ⇔ 0'
gen_s:0'5_0(+(x, 1)) ⇔ s(gen_s:0'5_0(x))
gen_cons:nil6_0(0) ⇔ nil
gen_cons:nil6_0(+(x, 1)) ⇔ cons(0', gen_cons:nil6_0(x))
gen_01':s17_0(0) ⇔ 01'
gen_01':s17_0(+(x, 1)) ⇔ s1(gen_01':s17_0(x))
gen_nil1:cons18_0(0) ⇔ nil1
gen_nil1:cons18_0(+(x, 1)) ⇔ cons1(01', gen_nil1:cons18_0(x))

No more defined symbols left to analyse.

(42) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)

(43) BOUNDS(n^1, INF)

(44) Obligation:

TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0') → 01'
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, Z)
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)

Types:
sel :: s:0' → cons:nil → s:0'
s :: s:0' → s:0'
cons :: s:0' → cons:nil → cons:nil
0' :: s:0'
first :: s:0' → cons:nil → cons:nil
nil :: cons:nil
from :: s:0' → cons:nil
sel1 :: s:0' → cons:nil → 01':s1
quote :: s:0' → 01':s1
first1 :: s:0' → cons:nil → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
01' :: 01':s1
quote1 :: cons:nil → nil1:cons1
s1 :: 01':s1 → 01':s1
unquote :: 01':s1 → s:0'
unquote1 :: nil1:cons1 → cons:nil
fcons :: s:0' → cons:nil → cons:nil
hole_s:0'1_0 :: s:0'
hole_cons:nil2_0 :: cons:nil
hole_01':s13_0 :: 01':s1
hole_nil1:cons14_0 :: nil1:cons1
gen_s:0'5_0 :: Nat → s:0'
gen_cons:nil6_0 :: Nat → cons:nil
gen_01':s17_0 :: Nat → 01':s1
gen_nil1:cons18_0 :: Nat → nil1:cons1

Lemmas:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)
first(gen_s:0'5_0(n464_0), gen_cons:nil6_0(n464_0)) → gen_cons:nil6_0(n464_0), rt ∈ Ω(1 + n464₀)
unquote(gen_01':s17_0(n945_0)) → gen_s:0'5_0(n945_0), rt ∈ Ω(1 + n945₀)
unquote1(gen_nil1:cons18_0(n1203_0)) → gen_cons:nil6_0(n1203_0), rt ∈ Ω(1 + n1203₀)
quote(gen_s:0'5_0(n2813_0)) → gen_01':s17_0(n2813_0), rt ∈ Ω(1 + n2813₀)
sel1(gen_s:0'5_0(n2282_0), gen_cons:nil6_0(+(1, n2282_0))) → gen_01':s17_0(0), rt ∈ Ω(1 + n2282₀)

Generator Equations:
gen_s:0'5_0(0) ⇔ 0'
gen_s:0'5_0(+(x, 1)) ⇔ s(gen_s:0'5_0(x))
gen_cons:nil6_0(0) ⇔ nil
gen_cons:nil6_0(+(x, 1)) ⇔ cons(0', gen_cons:nil6_0(x))
gen_01':s17_0(0) ⇔ 01'
gen_01':s17_0(+(x, 1)) ⇔ s1(gen_01':s17_0(x))
gen_nil1:cons18_0(0) ⇔ nil1
gen_nil1:cons18_0(+(x, 1)) ⇔ cons1(01', gen_nil1:cons18_0(x))

No more defined symbols left to analyse.

(45) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)

(46) BOUNDS(n^1, INF)

(47) Obligation:

TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0') → 01'
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, Z)
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)

Types:
sel :: s:0' → cons:nil → s:0'
s :: s:0' → s:0'
cons :: s:0' → cons:nil → cons:nil
0' :: s:0'
first :: s:0' → cons:nil → cons:nil
nil :: cons:nil
from :: s:0' → cons:nil
sel1 :: s:0' → cons:nil → 01':s1
quote :: s:0' → 01':s1
first1 :: s:0' → cons:nil → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
01' :: 01':s1
quote1 :: cons:nil → nil1:cons1
s1 :: 01':s1 → 01':s1
unquote :: 01':s1 → s:0'
unquote1 :: nil1:cons1 → cons:nil
fcons :: s:0' → cons:nil → cons:nil
hole_s:0'1_0 :: s:0'
hole_cons:nil2_0 :: cons:nil
hole_01':s13_0 :: 01':s1
hole_nil1:cons14_0 :: nil1:cons1
gen_s:0'5_0 :: Nat → s:0'
gen_cons:nil6_0 :: Nat → cons:nil
gen_01':s17_0 :: Nat → 01':s1
gen_nil1:cons18_0 :: Nat → nil1:cons1

Lemmas:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)
first(gen_s:0'5_0(n464_0), gen_cons:nil6_0(n464_0)) → gen_cons:nil6_0(n464_0), rt ∈ Ω(1 + n464₀)
unquote(gen_01':s17_0(n945_0)) → gen_s:0'5_0(n945_0), rt ∈ Ω(1 + n945₀)
unquote1(gen_nil1:cons18_0(n1203_0)) → gen_cons:nil6_0(n1203_0), rt ∈ Ω(1 + n1203₀)
quote(gen_s:0'5_0(n1846_0)) → gen_01':s17_0(n1846_0), rt ∈ Ω(1 + n1846₀)
sel1(gen_s:0'5_0(n2282_0), gen_cons:nil6_0(+(1, n2282_0))) → gen_01':s17_0(0), rt ∈ Ω(1 + n2282₀)

Generator Equations:
gen_s:0'5_0(0) ⇔ 0'
gen_s:0'5_0(+(x, 1)) ⇔ s(gen_s:0'5_0(x))
gen_cons:nil6_0(0) ⇔ nil
gen_cons:nil6_0(+(x, 1)) ⇔ cons(0', gen_cons:nil6_0(x))
gen_01':s17_0(0) ⇔ 01'
gen_01':s17_0(+(x, 1)) ⇔ s1(gen_01':s17_0(x))
gen_nil1:cons18_0(0) ⇔ nil1
gen_nil1:cons18_0(+(x, 1)) ⇔ cons1(01', gen_nil1:cons18_0(x))

No more defined symbols left to analyse.

(48) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)

(49) BOUNDS(n^1, INF)

(50) Obligation:

TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0') → 01'
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, Z)
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)

Types:
sel :: s:0' → cons:nil → s:0'
s :: s:0' → s:0'
cons :: s:0' → cons:nil → cons:nil
0' :: s:0'
first :: s:0' → cons:nil → cons:nil
nil :: cons:nil
from :: s:0' → cons:nil
sel1 :: s:0' → cons:nil → 01':s1
quote :: s:0' → 01':s1
first1 :: s:0' → cons:nil → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
01' :: 01':s1
quote1 :: cons:nil → nil1:cons1
s1 :: 01':s1 → 01':s1
unquote :: 01':s1 → s:0'
unquote1 :: nil1:cons1 → cons:nil
fcons :: s:0' → cons:nil → cons:nil
hole_s:0'1_0 :: s:0'
hole_cons:nil2_0 :: cons:nil
hole_01':s13_0 :: 01':s1
hole_nil1:cons14_0 :: nil1:cons1
gen_s:0'5_0 :: Nat → s:0'
gen_cons:nil6_0 :: Nat → cons:nil
gen_01':s17_0 :: Nat → 01':s1
gen_nil1:cons18_0 :: Nat → nil1:cons1

Lemmas:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)
first(gen_s:0'5_0(n464_0), gen_cons:nil6_0(n464_0)) → gen_cons:nil6_0(n464_0), rt ∈ Ω(1 + n464₀)
unquote(gen_01':s17_0(n945_0)) → gen_s:0'5_0(n945_0), rt ∈ Ω(1 + n945₀)
unquote1(gen_nil1:cons18_0(n1203_0)) → gen_cons:nil6_0(n1203_0), rt ∈ Ω(1 + n1203₀)
quote(gen_s:0'5_0(n1846_0)) → gen_01':s17_0(n1846_0), rt ∈ Ω(1 + n1846₀)

Generator Equations:
gen_s:0'5_0(0) ⇔ 0'
gen_s:0'5_0(+(x, 1)) ⇔ s(gen_s:0'5_0(x))
gen_cons:nil6_0(0) ⇔ nil
gen_cons:nil6_0(+(x, 1)) ⇔ cons(0', gen_cons:nil6_0(x))
gen_01':s17_0(0) ⇔ 01'
gen_01':s17_0(+(x, 1)) ⇔ s1(gen_01':s17_0(x))
gen_nil1:cons18_0(0) ⇔ nil1
gen_nil1:cons18_0(+(x, 1)) ⇔ cons1(01', gen_nil1:cons18_0(x))

No more defined symbols left to analyse.

(51) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)

(52) BOUNDS(n^1, INF)

(53) Obligation:

TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0') → 01'
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, Z)
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)

Types:
sel :: s:0' → cons:nil → s:0'
s :: s:0' → s:0'
cons :: s:0' → cons:nil → cons:nil
0' :: s:0'
first :: s:0' → cons:nil → cons:nil
nil :: cons:nil
from :: s:0' → cons:nil
sel1 :: s:0' → cons:nil → 01':s1
quote :: s:0' → 01':s1
first1 :: s:0' → cons:nil → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
01' :: 01':s1
quote1 :: cons:nil → nil1:cons1
s1 :: 01':s1 → 01':s1
unquote :: 01':s1 → s:0'
unquote1 :: nil1:cons1 → cons:nil
fcons :: s:0' → cons:nil → cons:nil
hole_s:0'1_0 :: s:0'
hole_cons:nil2_0 :: cons:nil
hole_01':s13_0 :: 01':s1
hole_nil1:cons14_0 :: nil1:cons1
gen_s:0'5_0 :: Nat → s:0'
gen_cons:nil6_0 :: Nat → cons:nil
gen_01':s17_0 :: Nat → 01':s1
gen_nil1:cons18_0 :: Nat → nil1:cons1

Lemmas:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)
first(gen_s:0'5_0(n464_0), gen_cons:nil6_0(n464_0)) → gen_cons:nil6_0(n464_0), rt ∈ Ω(1 + n464₀)
unquote(gen_01':s17_0(n945_0)) → gen_s:0'5_0(n945_0), rt ∈ Ω(1 + n945₀)
unquote1(gen_nil1:cons18_0(n1203_0)) → gen_cons:nil6_0(n1203_0), rt ∈ Ω(1 + n1203₀)

Generator Equations:
gen_s:0'5_0(0) ⇔ 0'
gen_s:0'5_0(+(x, 1)) ⇔ s(gen_s:0'5_0(x))
gen_cons:nil6_0(0) ⇔ nil
gen_cons:nil6_0(+(x, 1)) ⇔ cons(0', gen_cons:nil6_0(x))
gen_01':s17_0(0) ⇔ 01'
gen_01':s17_0(+(x, 1)) ⇔ s1(gen_01':s17_0(x))
gen_nil1:cons18_0(0) ⇔ nil1
gen_nil1:cons18_0(+(x, 1)) ⇔ cons1(01', gen_nil1:cons18_0(x))

No more defined symbols left to analyse.

(54) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)

(55) BOUNDS(n^1, INF)

(56) Obligation:

TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0') → 01'
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, Z)
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)

Types:
sel :: s:0' → cons:nil → s:0'
s :: s:0' → s:0'
cons :: s:0' → cons:nil → cons:nil
0' :: s:0'
first :: s:0' → cons:nil → cons:nil
nil :: cons:nil
from :: s:0' → cons:nil
sel1 :: s:0' → cons:nil → 01':s1
quote :: s:0' → 01':s1
first1 :: s:0' → cons:nil → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
01' :: 01':s1
quote1 :: cons:nil → nil1:cons1
s1 :: 01':s1 → 01':s1
unquote :: 01':s1 → s:0'
unquote1 :: nil1:cons1 → cons:nil
fcons :: s:0' → cons:nil → cons:nil
hole_s:0'1_0 :: s:0'
hole_cons:nil2_0 :: cons:nil
hole_01':s13_0 :: 01':s1
hole_nil1:cons14_0 :: nil1:cons1
gen_s:0'5_0 :: Nat → s:0'
gen_cons:nil6_0 :: Nat → cons:nil
gen_01':s17_0 :: Nat → 01':s1
gen_nil1:cons18_0 :: Nat → nil1:cons1

Lemmas:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)
first(gen_s:0'5_0(n464_0), gen_cons:nil6_0(n464_0)) → gen_cons:nil6_0(n464_0), rt ∈ Ω(1 + n464₀)
unquote(gen_01':s17_0(n945_0)) → gen_s:0'5_0(n945_0), rt ∈ Ω(1 + n945₀)

Generator Equations:
gen_s:0'5_0(0) ⇔ 0'
gen_s:0'5_0(+(x, 1)) ⇔ s(gen_s:0'5_0(x))
gen_cons:nil6_0(0) ⇔ nil
gen_cons:nil6_0(+(x, 1)) ⇔ cons(0', gen_cons:nil6_0(x))
gen_01':s17_0(0) ⇔ 01'
gen_01':s17_0(+(x, 1)) ⇔ s1(gen_01':s17_0(x))
gen_nil1:cons18_0(0) ⇔ nil1
gen_nil1:cons18_0(+(x, 1)) ⇔ cons1(01', gen_nil1:cons18_0(x))

No more defined symbols left to analyse.

(57) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)

(58) BOUNDS(n^1, INF)

(59) Obligation:

TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0') → 01'
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, Z)
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)

Types:
sel :: s:0' → cons:nil → s:0'
s :: s:0' → s:0'
cons :: s:0' → cons:nil → cons:nil
0' :: s:0'
first :: s:0' → cons:nil → cons:nil
nil :: cons:nil
from :: s:0' → cons:nil
sel1 :: s:0' → cons:nil → 01':s1
quote :: s:0' → 01':s1
first1 :: s:0' → cons:nil → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
01' :: 01':s1
quote1 :: cons:nil → nil1:cons1
s1 :: 01':s1 → 01':s1
unquote :: 01':s1 → s:0'
unquote1 :: nil1:cons1 → cons:nil
fcons :: s:0' → cons:nil → cons:nil
hole_s:0'1_0 :: s:0'
hole_cons:nil2_0 :: cons:nil
hole_01':s13_0 :: 01':s1
hole_nil1:cons14_0 :: nil1:cons1
gen_s:0'5_0 :: Nat → s:0'
gen_cons:nil6_0 :: Nat → cons:nil
gen_01':s17_0 :: Nat → 01':s1
gen_nil1:cons18_0 :: Nat → nil1:cons1

Lemmas:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)
first(gen_s:0'5_0(n464_0), gen_cons:nil6_0(n464_0)) → gen_cons:nil6_0(n464_0), rt ∈ Ω(1 + n464₀)

Generator Equations:
gen_s:0'5_0(0) ⇔ 0'
gen_s:0'5_0(+(x, 1)) ⇔ s(gen_s:0'5_0(x))
gen_cons:nil6_0(0) ⇔ nil
gen_cons:nil6_0(+(x, 1)) ⇔ cons(0', gen_cons:nil6_0(x))
gen_01':s17_0(0) ⇔ 01'
gen_01':s17_0(+(x, 1)) ⇔ s1(gen_01':s17_0(x))
gen_nil1:cons18_0(0) ⇔ nil1
gen_nil1:cons18_0(+(x, 1)) ⇔ cons1(01', gen_nil1:cons18_0(x))

No more defined symbols left to analyse.

(60) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)

(61) BOUNDS(n^1, INF)

(62) Obligation:

TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0') → 01'
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, Z)
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)

Types:
sel :: s:0' → cons:nil → s:0'
s :: s:0' → s:0'
cons :: s:0' → cons:nil → cons:nil
0' :: s:0'
first :: s:0' → cons:nil → cons:nil
nil :: cons:nil
from :: s:0' → cons:nil
sel1 :: s:0' → cons:nil → 01':s1
quote :: s:0' → 01':s1
first1 :: s:0' → cons:nil → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
01' :: 01':s1
quote1 :: cons:nil → nil1:cons1
s1 :: 01':s1 → 01':s1
unquote :: 01':s1 → s:0'
unquote1 :: nil1:cons1 → cons:nil
fcons :: s:0' → cons:nil → cons:nil
hole_s:0'1_0 :: s:0'
hole_cons:nil2_0 :: cons:nil
hole_01':s13_0 :: 01':s1
hole_nil1:cons14_0 :: nil1:cons1
gen_s:0'5_0 :: Nat → s:0'
gen_cons:nil6_0 :: Nat → cons:nil
gen_01':s17_0 :: Nat → 01':s1
gen_nil1:cons18_0 :: Nat → nil1:cons1

Lemmas:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)

Generator Equations:
gen_s:0'5_0(0) ⇔ 0'
gen_s:0'5_0(+(x, 1)) ⇔ s(gen_s:0'5_0(x))
gen_cons:nil6_0(0) ⇔ nil
gen_cons:nil6_0(+(x, 1)) ⇔ cons(0', gen_cons:nil6_0(x))
gen_01':s17_0(0) ⇔ 01'
gen_01':s17_0(+(x, 1)) ⇔ s1(gen_01':s17_0(x))
gen_nil1:cons18_0(0) ⇔ nil1
gen_nil1:cons18_0(+(x, 1)) ⇔ cons1(01', gen_nil1:cons18_0(x))

No more defined symbols left to analyse.

(63) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)

(64) BOUNDS(n^1, INF)